◀ Prev · Parts · Full

layout: Wide · Narrow · Centered

• TACO, an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.

• Gary T. Leavens and Yoonsik Cheon. Design by Contract with JML; Draft tutorial.

• Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design; in Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, Kluwer, 1999, chapter 12, pages 175-188.

• Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), September 2009. HTML

• Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. Formal specification with JML. 2014. download (CC-BY-NC-ND)

• JML website

◀ Prev · Parts · Full